/* domain
        Dom_Node = Node &        
        Dom_Empty = Empty
*/
  
sealed abstract class BT {
  def isZero(n: Int): Boolean = 
    /* postcondition res == true <--> n == 0
     */
     n == 0
  
 def isEmpty(t : BT): Boolean = 
   /* postcondition (res == true) <--> (t \in Empty)
    */
    t.isInstanceOf[Empty]

    
 def isNode1(): Boolean = (this : BT) match {
   case Node(_,_) if this.isZero(3) => true
   case Node(_,_) if !this.isZero(3) => true
   case Empty() => false
  }
    
 def isNode2(): Boolean = (this : BT) match {
   case Node(c: BT,d: BT) if this.isEmpty(c) => true
   case Node(c: BT,d: BT) if !this.isEmpty(c) => true
   case Empty() => false
 }
   
 def isNode3(): Boolean = (this : BT) match {
   case Node(a:BT,b: BT) if this.isEmpty(b) => true
   case Node(c: BT,d: BT) if this.isEmpty(c) && !this.isEmpty(d) => true
   case Node(c: BT,d: BT) if !this.isEmpty(c) && !this.isEmpty(d) => true
   case Empty() => false
 }
     
  
 
  
}
class Empty extends BT
class Node(val left: BT, val right: BT) extends BT

class Dummy(val b: Boolean) {}

object Node {
  
  def apply(left: BT, right: BT): Node = 
    new Node(left,right)
    
  def unapply(n: Node): Option[(BT,BT)] =
    Some(Tuple2(n.left,n.right))
}

object Empty {
  def apply(): Empty = new Empty()
  
  def unapply(e: Empty): Boolean =    
    e.isInstanceOf[Empty]
}

object Reachable {

  def main(args: Array[String]): Unit =
    Node(Node(Empty(),Empty()),Empty()).isNode()
}




